1. $A$ : Type
\\[0ex]2. $x$ : $A$
\\[0ex]3. $y$ : $A$
\\[0ex]4. $P$ : $A$$\rightarrow\mathbb{P}$
\\[0ex]5. $i$ : $\mathbb{Z}$
\\[0ex]6. $j$ : $\mathbb{Z}$
\\[0ex]7. $P$(if ($i$ =$_{0}$ $j$) then $x$ else $y$ fi )
\\[0ex]8. $\mathbb{B}$ $\in$ Type
\\[0ex]9. ($i$ =$_{0}$ $j$) $\in$ $\mathbb{B}$
\\[0ex]10. $\forall$${\it bb}$:$\mathbb{B}$. (($i$ =$_{0}$ $j$) = ${\it bb}$) $\in$ Type
\\[0ex]$\vdash$  ($i$ =$_{0}$ $j$) = ($i$ =$_{0}$ $j$)